$\forall$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), $m$:Msg($M$). mtag($m$) $\in$ Id